Section: New Results

Models of Programming

• P. Herms, together with C. Marché and B. Monate (CEA List), developed a certified VC generator, using Coq. The program for VC calculus and its specifications are both written in Coq, but the code is crafted so that it can be extracted automatically into a stand-alone executable. It is also designed in a way that allows the use of arbitrary first-order theorem provers to discharge the generated obligations [37] . This is a first step towards a certified VC generator for C programs annotated with ACSL  [54] .

• Until now, we only considered the proof of sequential programs. However the rely/guarantee approach give a natural way to extend deductive verification to concurrent programs. During his internship supervised by C. Paulin, N. Gaspar explored this idea. He formalised in Coq the axiomatic semantics of a simple concurrent language using the rely-guarranty approach [43] and proposed a translation of this language into Why programs in order to automatically generate the proof obligations.

• W. Urribarrí, together with C. Paulin, proposed an extension of the Why language with modules and functors together with a refinement calculus in order to organise large developments in a structured and abstract way. She built a prototype implementation of this calculus.

• D. Baelde, in cooperation with P. Courtieu (CNAM), D. Gross-Amblard (U. Bourgogne and Rennes), C. Paulin and X. Urbain proposed a formal proof of security for two watermarking algorithms. The proof uses a reduction of an arbitrary attack unmarking the data to the discovery of a secret key. It has been fully formalized in Coq using the ALEA library. This work has been presented at the conference TYPES 2011 and a paper is in preparation.

• Generating multimedia streams, such as in a netradio, is a task which is complex and difficult to adapt to every users' needs. D. Baelde, in cooperation with R. Beauxis (Tulane University, LA, USA) and S. Mimram (CEA List) introduce a novel approach, based on a dedicated high-level functional programming language, called Liquidsoap, for generating, manipulating and broadcasting multimedia streams [20] . Unlike traditional approaches, which are based on configuration files or static graphical interfaces, it also allows the user to build complex and highly customized systems. This language is based on a model for streams and contains operators and constructions, which make it adapted to the generation of streams. The interpreter of the language also ensures many properties concerning the good execution of the stream generation.